Lean 4 ログ
2024-08-04
『Theorem Proving in Lean 4』
量化子と等号 - Theorem Proving in Lean 4 日本語訳
帰納と再帰 - Theorem Proving in Lean 4 日本語訳
公理と計算 - Theorem Proving in Lean 4 日本語訳
Calculus of Inductive Constructions(CIC)
証明無関係(proof irrelevance)
opaqueタクティク
非可述的性(impredicative)
have(Lean)
dsimp
dsimp: 定義に展開 - Lean by Example
定義上(definitionally)等しいような変形だけを行うという制約付きの simp
@pred: 暗黙の引数を表示させる
assumption
choice principle(選択原理)
ラッセルのパラドクスとはまた違うジラールのパラドックス(Girard's paradox)があることが分かった
code:memo
命題外延性の公理 propext
商型 Quot の構築 : 関数外延性 funext を含意する
選択原理 Classical.choice : 存在命題 Nonempty α からデータ a : α を生成する
propext, funext
setext
命題論理に帰着させる
Eq.reqOn
帰納法
motiveタクティク
Observational Type Theory
同値類
商型Quot
Quot.mk
Quot.sound
Setoid
同値型がくっついた型クラス